Inference at * 1 
Iof proof for Lemma inconsistent-bool-eq:



1. tt = ff
  False 

latex

 by (Unfolds ``btrue bfalse bool`` ( -1)) 
CollapseTHEN ((ApFunToHypEquands `Z' case Z
Cof inl(x) => 0
Co| inr(x) => 1  (-1)) 
CollapseTHEN (Auto)) 

latex

C1: 

C1: 1. (inl  ) = (inr  )
C1: 2. case inl   of inl(x) => 0 | inr(x) => 1 = case inr   of inl(x) => 0 | inr(x) => 1
C1:   False
C.

Definitions	case b of inl(x) => s(x) | inr(y) => t(y), #$n, , , tt, ff, left + right, Unit, False, Void
Lemmas	unit wf